System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning
Identifieur interne : 002168 ( Main/Exploration ); précédent : 002167; suivant : 002169System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning
Auteurs : Jürgen Zimmer [Allemagne] ; Michael Kohlhase [États-Unis]Source :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2002.
Abstract
Abstract: Automated reasoning systems have reached a high degree of maturity in the last decade. Many reasoning tasks can be delegated to an automated theorem prover (ATP) by encoding them into its interface logic, simply calling the system and waiting for a proof, which will arrive in less than a second in most cases. Despite this seemingly ideal situation, ATPs are seldom actually used by people other than their own developers. The reasons for this seem to be that it is difficult for practitioners of other fields to find information about theorem prover software, to decide which system is best suited for the problem at hand, installing it, and coping with the often idiosyncratic concrete input syntax. Of course, not only potential outside users face these problems, so that, more often than not, existing reasoning procedures are re-implemented instead of re-used.
Url:
DOI: 10.1007/3-540-45620-1_11
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000763
- to stream Istex, to step Curation: 000607
- to stream Istex, to step Checkpoint: 001A35
- to stream Main, to step Merge: 002214
- to stream Main, to step Curation: 002168
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct:series"><teiHeader><fileDesc><titleStmt><title xml:lang="en">System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning</title><author><name sortKey="Zimmer, Jurgen" sort="Zimmer, Jurgen" uniqKey="Zimmer J" first="Jürgen" last="Zimmer">Jürgen Zimmer</name></author><author><name sortKey="Kohlhase, Michael" sort="Kohlhase, Michael" uniqKey="Kohlhase M" first="Michael" last="Kohlhase">Michael Kohlhase</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:3EB101D27C2A4D38EBFFBF1ADEBE68EAD3ACAB96</idno><date when="2002" year="2002">2002</date><idno type="doi">10.1007/3-540-45620-1_11</idno><idno type="url">https://api.istex.fr/document/3EB101D27C2A4D38EBFFBF1ADEBE68EAD3ACAB96/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">000763</idno><idno type="wicri:Area/Istex/Curation">000607</idno><idno type="wicri:Area/Istex/Checkpoint">001A35</idno><idno type="wicri:doubleKey">0302-9743:2002:Zimmer J:system:description:the</idno><idno type="wicri:Area/Main/Merge">002214</idno><idno type="wicri:Area/Main/Curation">002168</idno><idno type="wicri:Area/Main/Exploration">002168</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning</title><author><name sortKey="Zimmer, Jurgen" sort="Zimmer, Jurgen" uniqKey="Zimmer J" first="Jürgen" last="Zimmer">Jürgen Zimmer</name><affiliation wicri:level="1"><country xml:lang="fr">Allemagne</country><wicri:regionArea>FB Informatik, Universität des Saarlandes</wicri:regionArea><wicri:noRegion>Universität des Saarlandes</wicri:noRegion><wicri:noRegion>Universität des Saarlandes</wicri:noRegion></affiliation><affiliation><wicri:noCountry code="no comma">E-mail: jzimmer@mathweb.org</wicri:noCountry></affiliation></author><author><name sortKey="Kohlhase, Michael" sort="Kohlhase, Michael" uniqKey="Kohlhase M" first="Michael" last="Kohlhase">Michael Kohlhase</name><affiliation wicri:level="4"><country xml:lang="fr">États-Unis</country><wicri:regionArea>School of Computer Science, Carnegie Mellon University</wicri:regionArea><placeName><settlement type="city">Pittsburgh</settlement><region type="state">Pennsylvanie</region></placeName><orgName type="university">Université Carnegie-Mellon</orgName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">États-Unis</country></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2002</date></imprint><idno type="ISSN">0302-9743</idno></series><idno type="istex">3EB101D27C2A4D38EBFFBF1ADEBE68EAD3ACAB96</idno><idno type="DOI">10.1007/3-540-45620-1_11</idno><idno type="ChapterID">Chap11</idno><idno type="ChapterID">11</idno></biblStruct></sourceDesc></fileDesc><profileDesc><textClass></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Automated reasoning systems have reached a high degree of maturity in the last decade. Many reasoning tasks can be delegated to an automated theorem prover (ATP) by encoding them into its interface logic, simply calling the system and waiting for a proof, which will arrive in less than a second in most cases. Despite this seemingly ideal situation, ATPs are seldom actually used by people other than their own developers. The reasons for this seem to be that it is difficult for practitioners of other fields to find information about theorem prover software, to decide which system is best suited for the problem at hand, installing it, and coping with the often idiosyncratic concrete input syntax. Of course, not only potential outside users face these problems, so that, more often than not, existing reasoning procedures are re-implemented instead of re-used.</div></front></TEI><affiliations><list><country><li>Allemagne</li><li>États-Unis</li></country><region><li>Pennsylvanie</li></region><settlement><li>Pittsburgh</li></settlement><orgName><li>Université Carnegie-Mellon</li></orgName></list><tree><country name="Allemagne"><noRegion><name sortKey="Zimmer, Jurgen" sort="Zimmer, Jurgen" uniqKey="Zimmer J" first="Jürgen" last="Zimmer">Jürgen Zimmer</name></noRegion></country><country name="États-Unis"><region name="Pennsylvanie"><name sortKey="Kohlhase, Michael" sort="Kohlhase, Michael" uniqKey="Kohlhase M" first="Michael" last="Kohlhase">Michael Kohlhase</name></region><name sortKey="Kohlhase, Michael" sort="Kohlhase, Michael" uniqKey="Kohlhase M" first="Michael" last="Kohlhase">Michael Kohlhase</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Musique/explor/MozartV1/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002168 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 002168 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Musique
|area= MozartV1
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:3EB101D27C2A4D38EBFFBF1ADEBE68EAD3ACAB96
|texte= System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning
}}
| This area was generated with Dilib version V0.6.20. |  |